(DEFPROP GOAL
 (NIL ((term . t1hdterm)
       (terms . t1tlterms)
       (term . t2hdterm)
       (terms . t2tlterms)
       (subst . s))
      ((: (pair_unify (apply s t1hdterm) (apply s t2hdterm)) subst)
       (: (apply s t2hdterm) term)
       (: (apply s t1hdterm) term)
       (: (apply s (multterm t2hdterm t2tlterms)) multterm)
       (: (apply s (multterm t1hdterm t1tlterms)) multterm))
      ((((terms . &t1) (terms . &t2) (subst . &s))
	((⊂ &t1 (multterm t1hdterm t1tlterms)))
	NIL
	(∨ (= (apply (unify (apply &s &t1) (apply &s &t2)) (apply &s &t1))
	      (apply (unify (apply &s &t1) (apply &s &t2)) (apply &s &t2)))
	   (= (unify (apply &s &t1) (apply &s &t2)) 'NOSUBST))))
      (∨ (= (apply (unify2 (pair_unify (apply s t1hdterm)
				       (apply s t2hdterm))
			   (unify (apply (pair_unify (apply s t1hdterm)
						     (apply s t2hdterm))
					 (apply s t1tlterms))
				  (apply (pair_unify (apply s t1hdterm)
						     (apply s t2hdterm))
					 (apply s t2tlterms))))
		   (apply s (multterm t1hdterm t1tlterms)))
	    (apply (unify2 (pair_unify (apply s t1hdterm)
				       (apply s t2hdterm))
			   (unify (apply (pair_unify (apply s t1hdterm)
						     (apply s t2hdterm))
					 (apply s t1tlterms))
				  (apply (pair_unify (apply s t1hdterm)
						     (apply s t2hdterm))
					 (apply s t2tlterms))))
		   (apply s (multterm t2hdterm t2tlterms))))
	 (= (unify2 (pair_unify (apply s t1hdterm) (apply s t2hdterm))
		    (unify (apply (pair_unify (apply s t1hdterm)
					      (apply s t2hdterm))
				  (apply s t1tlterms))
			   (apply (pair_unify (apply s t1hdterm)
					      (apply s t2hdterm))
				  (apply s t2tlterms))))
	    'NOSUBST)))
VALUE)